\section{Finding Permanent Workaround with Alloy and Dynalloy}\label{propuesta}
%El proceso de debugging se ha convertido en una de las actividades m\'as importantes dentro del proceso de desarrollo de un sofware.
The debugging process is one of the most important activities in the development process.
%Se define debugging como la b\'usqueda, aislamiento y correci\'on de defectos del software. Este proceso se divide en tres actividades reproducci\'on del error, determinaci\'on de posibles causas y aislamiento de las mismas, y finalmente, correcci\'on del error.  
Debugging is defined as the search, isolation and correction of software defects. 
%Este proceso se divide en tres actividades reproducción del error, determinación de posibles causas y aislamiento de las mismas, y finalmente, corrección del error.  
This process is composed of the following activities: reproduction of the error, determination of possible causes and isolation of the same ones, and finally, correction of the error.
%La idea general de este trabajo se fundamenta en la utilización del concepto de workarounds para asistir al desarrollador dentro de la actividad de debugging. 
The success of the testing and debungging depends of the skill of the tester or programmer.
%El programador realiza la codificación de un programa P formado por una secuencia de acciones a1...an con sus respectivos contratos pre y post-condiciones.
Our proposal uses the workarounds concept to define a technique that helps to developer during the debugging task.
%Para ello necesitamos  contar con los contratos pre y post condiciones de cada procedimiento involucrado en el desarrollo. 
The developer write a program \textit{$P$}, it consists in a sequence of actions\textit{ \{$a_{1}$,...,$a_{n}$\}}.
%Cada acción debe proveer  su contrato a través de una pre y post-condiciones
Every action must provide your contract through \textit{$pre$} and \textit{$post-conditions$}.
For many causes, the code written by the programmer may have errors. Syntactic errors are the simplest to correct. 
Programming languages ​​provide tools for detection and suggest possible solutions.
The behavior errors are more hard of to detect and to fix. The program is syntactically correct but, it produces a wrong output.\\ 
The first step for to fix the fail is detect the action \textit{\{$a_{j}$\}} that caused the error. The next step will 
be to find a workarround (a new action sequence \textit{P'}), without the action\textit{\{$a_{j}$\}}. The workaround 
\textit{$P'$} will have to verify the contract of \textit{$P$}.\\
In this work, we present an algorithm to find permanent workarounds using Alloy and Dynalloy. \\
The algorithm is defined in pseudo-code and take as parameters a \textit{$P$} program and an \textit{\{$a_{k}$\}} action.
\textit{$P$} is the program that produces a wroung output because it had run the \textit{\{$a_{k}$\}} action. 

\begin{verbatim}
Procedure Find_PWa(P:Program, ak:Action)
 Begin 
 1.  j = limit of CWa to find
 2.  count = 0 
 3.  Q is the pre-condition of P program 
 4.  R is the post-contition of P program 
 5.  exit:= false
 6.  Repeat
 7.     P':=  {a1 + a2 +...+ an}*, It's exclude the action ak that cause the error
 8.     if  Dynalloy(Q,P',R) then
 9.              print 'P' is a PWa ' 
 10.             exit:=true
 11.    else
 12.             eject P' 
 13.    count:=count + 1
 14. Until(count >=j or exit)
end;
\end{verbatim}

See some details of the above algorithm.
The general idea is use Dynalloy tool for generate the CWa $P'$, that exclude the action ak(cause of fault). The CWa is 
generated with the operator no deterministic $+$. $P'$ is verified in line 8 for all values asignement to variable's program. 
If exist some execution trace that not verifies the contract ${Q , S}$, then $P'$ isn't a PWa. Otherwise, 
$P'$ is a \textit{$PWa$} and it will be able to be used for fix the bug.\\
In the next section, we show a case of study.

HABRIA QUE EXPLICAR MAS EL ALGORITMO????








 

 